Circuit designs (e.g., for computer hardware) are normally verified before being fabricated. During verification, a design is sometimes referred to as a design under test (DUT). Typically, a DUT is verified by running a simulation program on a computer during which different inputs (called stimuli, inputs, or events) are in turn applied to the DUT, and the signals at the outputs of the DUT are collected and compared with expected values of the design specification. When actual output values of the DUT do not agree with predicted values of the design specification, the circuit design is considered defective and is usually re-designed.
Often times, a particular input to a DUT yields a single, predictable output. For example, input A results in output X, while input B results in output Y. Conventional verification software often very straightforwardly compares a predicted output to the actual output of the DUT as the simulation time advances.
Sometimes, however, the specification of the circuit design defines multiple outcomes when an event occurs within a specific time frame, such that the verification software cannot predict definitive behavior. For example, input A might validly result in either output X or Y. Put another way, as a set of inputs propagate (e.g., race) through the DUT, more than one valid output might be predicted. In such cases, the DUT is said to exhibit non-deterministic behavior. It is difficult to verify DUT's that exhibit non-deterministic behavior, since a given input may result in more than one different output.
An example of non-deterministic behavior is embodied in the PCI-Express Transaction Layer design, which manages buffer space for packet transmission and reception. If the buffer is overwritten by packets that exceed the allocated buffer space, an overflow error is reported by the circuit (also referred to as the core). The allocated buffer space is freed by the processing of received packets by higher layers in the PCI-Express Stack. If buffer space is freed around the time a packet is received that would cause an overflow, depending upon the logic implementation and amount of pipelining in the core, the buffer overflow error may (or may not) be reported. Either outcome is correct behavior based upon the specification as long as the two events occurred within a specific amount of time relative to each other.
Some state machines that are internal to a DUT represent another example of non-deterministic behavior. Since the entire state machine is typically treated as a black box, the verifiers only have access to two items: the inputs going into the DUT and the outputs coming from the DUT. There is no access to the actual state the DUT is in at any given time.
A common way to verify a black box state machine is to build an external model that implements the same states, and is given the same stimulus as the DUT. If at any time the outputs of the DUT are different from the outputs of the model, then it is said that the DUT (or model) has made an invalid transition or is behaving inappropriately (based on the design specifications).
However, there are many problems with this approach. The implementation of the two state machines (the DUT and the model) can be very different. One could pipeline incoming data so it sees inputs at a different point in time than the other. This would cause the outputs to be different at a given time, but neither state machine is wrong. Many false fails will be found this way, and a lot of time is normally spent trying to match the model to the DUT implementation.
Another conventional design pattern that is sometimes used for verifying state machines is known as the “State” pattern. This pattern is commonly used in object oriented programming and describes a method of partitioning a function that is state dependant into several discrete classes, all of which inherit from a common parent class, allowing them to be used interchangeably. While this method of representing state based behavior is robust and maintainable, it requires that only one state is considered valid at any one-time. This limitation is a problem when attempting to verify a DUT that exhibits non-deterministic behavior.
Accordingly, there exists a need in the art to overcome the deficiencies and limitations described hereinabove.